\begin{tabbing}
$\forall$${\it es}$:ES, $x$, ${\it free}$:Id, $e$:E.
\\[0ex]@loc($e$)($x$:Id)
\\[0ex]$\Rightarrow$ ($\neg$(($x$ after $e$) = ($x$ when $e$) $\in$ Id))
\\[0ex]$\Rightarrow$ (0 $<$ round($e$))
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:E\+
\\[0ex](${\it e'}$ $\leq$loc $e$ 
\\[0ex]\& rank(${\it e'}$) = $<$round($e$), 0$>$ $\in$ (:$\mathbb{N}$ $\times$ $\mathbb{N}$)
\\[0ex]\& ($\neg$(($x$ after ${\it e'}$) = ($x$ when ${\it e'}$) $\in$ Id))))
\-
\end{tabbing}